T:Type, n:, f:(nT), i:n. (f{n})[i] = f(i) 

latex

Definitions	{i..j}, x:A. B(x), , t  T, {...i}, P  Q, AB, l[i], f{m..n}, x. t(x), {T}, Prop, ||as||, S  T, A, False, S  T, i  j < k, P & Q, Unit, P  Q, P  Q, T, ij, , b, b, i<j, True, Dec(P), P  Q
Lemmas	select cons tl, select cons hd, decidable int equal, lt int wf, assert wf, bnot wf, bool wf, le int wf, assert of lt int, bnot of le int, true wf, squash wf, eqff to assert, iff transitivity, assert of le int, eqtt to assert, int lower wf, le wf, listify wf, length wf1, listify length, select wf, int lower ind, nat wf, int seg wf